./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_max -const N=1000,K=8,reset=false
PRISM
=====
Version: 4.5.dev
Date: Sun Mar 15 03:01:25 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 zeroconf.prism zeroconf.props --property correct_max -const 'N=1000,K=8,reset=false'
Parsing model file "zeroconf.prism"...
Type: MDP
Modules: environment host0
Variables: b_ip7 b_ip6 b_ip5 b_ip4 b_ip3 b_ip2 b_ip1 b_ip0 n n0 n1 b z ip_mess x y coll probes mess defend ip l
Parsing properties file "zeroconf.props"...
2 properties:
(1) "correct_max": Pmax=? [ F (l=4&ip=1) ]
(2) "correct_min": Pmin=? [ F (l=4&ip=1) ]
---------------------------------------------------------------------
Model checking: "correct_max": Pmax=? [ F (l=4&ip=1) ]
Model constants: reset=false,N=1000,K=8
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Model constants: reset=false,N=1000,K=8
Computing reachable states...
Reachability (BFS): 592 iterations in 69.25 seconds (average 0.116976, setup 0.00)
Time for model construction: 70.203 seconds.
Type: MDP
States: 1870338 (1 initial)
Transitions: 4245554
Choices: 3443961
Transition matrix: 154038 nodes (6 terminal), 4245554 minterms, vars: 58r/58c/7nd
Prob0A: 131 iterations in 4.26 seconds (average 0.032496, setup 0.00)
Prob1E: 2127 iterations in 93.81 seconds (average 0.044103, setup 0.00)
yes = 171749, no = 611330, maybe = 1087259
Computing remaining probabilities...
Engine: Sparse
Building quotient MDP, collapsing maximal end components as well as yes and no states...
Time for computing maximal end components: 3.702 seconds, found 0 MECs.
Time for building MEC quotient: 13.525 seconds.
Quotient MDP:
States: 1087261 (1 initial)
Transitions: 3619193
Choices: 3139484
Transition matrix: 1267651 nodes (6 terminal), 3619193 minterms, vars: 58r/58c/66nd
Note: Interval iteration is configured to enforce monotonicity from below.
Building sparse matrix... [n=1087261, nc=1997482, nnz=2477184, k=4] [31.3 MB]
Creating vector for yes... [8.3 MB]
Creating vector for maybe... [8.3 MB]
Allocating iteration vectors... [4 x 8.3 MB]
TOTAL: [81.1 MB]
Starting iterations (interval iteration)...
Iteration 122: max relative diff=1.000000, 5.00 sec so far
Iteration 245: max relative diff=0.999797, 10.03 sec so far
Iteration 372: max relative diff=0.660420, 15.07 sec so far
Iteration 501: max relative diff=0.013927, 20.10 sec so far
Iteration 631: max relative diff=0.000004, 25.11 sec so far
Max relative diff between upper and lower bound on convergence: 9.85426E-07
Iterative method (interval iteration): 664 iterations in 29.70 seconds (average 0.039729, setup 3.32)
Value in the initial state: 4.801413635072433E-8
Time for model checking: 149.566 seconds.
Result: 4.801413635072433E-8 (value in the initial state)
Overall running time: 220.384 seconds.
---------------------------------------------------------------------
Note: There was 1 warning during computation.